package datatableaux;

import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Stack;

import datatableaux.rules.*;

import entities.Assertion;
import entities.ConceptAssertion;
import entities.Individual;
import entities.concept.*;
import kb.*;

public class DataCompletion {
	
	public static final int INQUEUEFIRST = 0;
	public static final int INQUEUELAST = 1;

	private TBox tb;
	private ABox ab;
	private DataGraph dg;
	private Assertion ast;
	private DataBranching currentBranch;
	private Stack<DataBranching> allBranchesInPath;
	public Stack<DataBranching> getAllBranchesInPath() {
		return allBranchesInPath;
	}

	private LinkedList<Individual> individualsInQueue;
	private ClashTrigger clashtrigger ;
	private HashSet<Individual> allReasonedInds = new HashSet<Individual>();
	
	private void init(){
		this.currentBranch = null;
		this.allBranchesInPath = new Stack<DataBranching>();
		this.individualsInQueue = new LinkedList<Individual>();
	}
	
	/**
	 * when the parameter assertion is null, this checks the consistency of the ABox
	 * @param tb
	 * @param ab
	 * @param c
	 * @param as
	 */
	public DataCompletion(TBox tb, ABox ab, Assertion as) {
		init();
		if(tb == null){
			tb = new TBox();
		}
		if(ab == null){
			ab  = new ABox();
		}
		this.tb = tb;
		this.ab = ab;
		this.ast = as;
		this.clashtrigger = new ClashTrigger(this.tb);
	}
	/**
	 * 
	 * check if A is consistent.
	 * @return
	 */
	public boolean checkABoxConsistency(){
		boolean cons = false;
		this.dg = new DataGraph(this, ab);
		this.dg.ABox2DataGraph();
		
		if(ast != null && ast instanceof ConceptAssertion){
			ConceptAssertion ca = ast.asConceptAssertion();
			allReasonedInds.add(ca.getIndividual());
			Concept c = preprocessor.Simplification.NNF(ca.getConcept(), false);
			ast = new ConceptAssertion(ca.getIndividual(), c);
			this.dg.addNewAssertion(ast);
		}
		//Collection<Individual> inds = Individual.getAllIndividuals().values();
		//Collection<Individual> inds = this.ab.getABoxIndividuals();
		if(allReasonedInds == null || allReasonedInds.size()<1){
			return true;
		}
		this.individualsInQueue .addAll(allReasonedInds);
		//Collections.sort(this.individualsInQueue);
		//displayLabels(this.individualsInQueue);
		Individual root = this.individualsInQueue.getFirst();
		//this.individualsInQueue.addFirst(root);
		DataBranchChanges.setRecordingStatus(false);
		if(clashtrigger.clashFound(root)){
			root.isSat = false;
			cons = false;
			this.individualsInQueue.remove(root);
			return cons;
		}
		//start processing the individual queue
		while(!this.individualsInQueue .isEmpty()){
			Individual expind = this.individualsInQueue.peek();
			if(expind.blocked()){
				this.individualsInQueue.remove(expind);
				continue;
			}
			this.applyGCIs(expind);
			boolean initsat = this.expansion(expind);
			if(!initsat){
				if(!backtracking(expind)){
//					System.err.println("Clash found, individual labels:");
//					for(Concept c:expind.getLabels()){
//						System.out.println(c);
//					}
//					System.err.println("branches current:"+this.currentBranch);
//					System.err.println("branches stack:"+this.allBranchesInPath);
					cons = false;
					expind.isSat = false;
					//clean up global vars
					this.allBranchesInPath.clear();
					this.individualsInQueue.clear();
					return cons;
				}else{
					//still got branches to go
					continue;
				}
			}else{
				cons = true;
				//clean up global vars
				this.allBranchesInPath.clear();
				this.individualsInQueue .remove(expind);
			}
			
		}
		for(Individual ind:allReasonedInds){
			cons &= ind.isSat;
			//System.out.println("instance "+ind+": "+ind.isSat);
			if(!cons){
				return cons;
			}
		}
		return cons;
	}
	
	public static void displayLabels(Collection<Individual> my){
		//preserve the orders
		if(my instanceof LinkedList){
			LinkedList<Individual> x = (LinkedList<Individual>) my;
			for(int i =0; i<x.size(); i++){
				System.out.println("index "+i+", value: "+ x.get(i)+", its order: "+x.get(i).getOrder());
			}
		}else{
		for(Individual ind:my){
			System.out.println("====Display====\n\n"+ind.toString() + " -> "+ind.getLabels());
		}
		}
	}
	private boolean backtracking(Individual expind) {
		return this.hasNextBranch(expind);
	}

	//check if the individual has another choice for completion
	private boolean hasNextBranch(Individual expind) {
    	boolean has = false;
        if(currentBranch == null){
        	return false;
        }
      //only if the branches have this node or its ancestors as the branching node
        if(!currentBranch.noChoices()){
        	if(expind.equals(currentBranch.getBranchInd())){
                currentBranch.restore();
                modifyQueueContent(currentBranch);
                currentBranch.createBranch();
                has = true;
            }else if(expind.hasThisAncestor(currentBranch.getBranchInd())){
            	//if the current branch belongs to one of this node's ancestors, check if this node is
            	//produced by that ancestor, i.e., this node is created by exists rule anonymously.
//            	if(this.ab.getABoxIndividuals().contains(expind)){
//            		//this node is a given named individual
//            		return false;
//            	}
            	//an anonymous ind
            	currentBranch.restore();
            	modifyQueueContent(currentBranch);
                currentBranch.createBranch();
                has = true;      	
            }
        }else{
        	has = false;
        	//note that when previous branch is closed, the last added label is still there! We have to remove it.
        	this.currentBranch.getBranchInd().removeLabels(this.currentBranch.getLastChosenConcept());
        	//see if any upper level branches
            if(!this.allBranchesInPath.empty()){	
            	for(int i = 0; i<this.allBranchesInPath.size(); i++){
            		DataBranching br = this.allBranchesInPath.remove(i);     		
            		//if(currentBranch.getBranchInd().hasThisAncestor(br.getBranchInd())){
            		if(currentBranch.getFatherBranch() != null && currentBranch.getFatherBranch().equals(br)){
            			//currentBranch.restore();
            			currentBranch = br;
                        has = this.hasNextBranch(currentBranch.getBranchInd());
                        break;
            		}else{
            			this.allBranchesInPath.add(i, br);
            		}
            	}//end of for
            }else if(this.currentBranch.getFatherBranch() != null){
            	//no branches in stack, but this branch has father branches
            	currentBranch = this.currentBranch.getFatherBranch();
                has = this.hasNextBranch(currentBranch.getBranchInd());
            }
        }
        if(has){  
        	//if next branch available, clear the queue, add the branching node to expand again
        	//individualsInQueue.clear();
        	//System.err.println("Current Branch:"+currentBranch+"; #StackBranches:"+this.allBranchesInPath);
        	if(!this.individualsInQueue.contains(currentBranch.getBranchInd())){
        		this.addToQueue(currentBranch.getBranchInd(),  INQUEUELAST);
        	}
        	
        }
        return has;
	}

 

	private void modifyQueueContent(DataBranching br) {
		//previously, all inds in the queue are cleared.
		for(Individual ind:br.getBranchChanges().getPotentialQueueInds()){
			this.individualsInQueue.remove(ind);
		}
		br.getBranchChanges().clearPotentialQueueInds();
	}

	public boolean expansion(Individual expind){
		if(clashtrigger.clashFound(expind)){
			return false;
		}
		boolean moreRules = true;
		boolean changed = false;//if changed, then the current node needs to be re-expanded
		boolean presat = true;
		while( !expind.isCompleted() && moreRules){
			changed = false;
			DataAndRule cr = new DataAndRule(this);
			DataOrRule dr = new DataOrRule(this);
			DataSomeRule er = new DataSomeRule(this);
			DataAllRule fr = new DataAllRule(this);
			DataUnfoldingRule ar = new DataUnfoldingRule(this);
			if(cr.isApplicable(expind)){
				//no new node created
				//rules applied, labels changed.
				changed |= cr.applyRule(expind);
			}else
			if(fr.isApplicable(expind)){
				//no new nodes, forall won't change the labels of current node (consider no inverse roles)
				changed |= fr.applyRule(expind);
			}else
			if(ar.isApplicable(expind)){
				//more labels may be added to current node
				changed |= ar.applyRule(expind);
			}else
			if (dr.isApplicable(expind)){
				//add branching node to the queue, n is changed by adding a branch label
				changed |= dr.applyRule(expind);
			}else
			if(er.isApplicable(expind)){
				//if changed is true, then the current node is modified by adding the domain of the role!
				changed |= er.applyRule(expind);
			}		
			if(changed){
				//if changed, the node has to be expanded again!
				presat = !clashtrigger.clashFound(expind);
				if(!presat){
					return presat;
				}
			}
			else if(!expind.anyMoreRules(this)){
				//not changed, no more rules
				//add binary expanded to expandedLabels, s.t. expandedLabels will equal to
				//original labels
				moreRules = false;
				expind.addBinaryToExpandedLabels();
				presat = !clashtrigger.clashFound(expind);
				if(presat){
					//System.out.println(expind.getLabels());
				}
			}
		}
		return presat;
	}
	
	public void applyGCIs(Individual n){
		HashSet<Concept> newLabels = new HashSet<Concept>();
		for(Concept k:this.tb.getTg().keySet()){
			if(k.isTop()){
				newLabels.add(this.tb.getTg().get(k));
			}else{
				// c->d  -> ~c or d
				newLabels.add(new OrConcept(new NotConcept(k), this.tb.getTg().get(k)));
			}
		}
		n.addLabels(newLabels);
	}
	
	public DataBranching getCurrentBranching(){
		return this.currentBranch;
	}
	
	//a completion only has one data graph at a time
	public DataGraph getCurrentDataGraph(){
		return this.dg;
	}
	
	public TBox getInitTBox(){
		return this.tb;
	}
	
	public ABox getInitABox(){
		return this.ab;
	}
	
	//add an individual to the completion queue
	public void addToQueue(Individual n, int order){
		if(order == INQUEUEFIRST){
			this.individualsInQueue.addFirst(n);
			this.allReasonedInds.add(n);
			
		}else if(order == INQUEUELAST){
			this.individualsInQueue.addLast(n);
			this.allReasonedInds.add(n);
		}
		//order does not matter. as the queue will be sorted anyway!
		//Collections.sort(this.individualsInQueue);
	}

	public void addAsCurrentBranch(DataBranching br) {
		if(this.currentBranch != null){
//			if(this.allBranchesInPath.contains(this.currentBranch)){
//				this.allBranchesInPath.push(this.currentBranch);
//			}
			this.allBranchesInPath.push(this.currentBranch);
		}
		this.currentBranch = br;
	}
	
	public LinkedList<Individual> getIndQueue (){
		return this.individualsInQueue;
	}
	
}
